Nuprl Lemma : name-case_wf
11,40
postcript
pdf
T
:Type,
A
:(
i
:Id
{
k
:Knd|
hasloc(
k
;
i
)}
T
),
B
:(Id
Id
T
),
n
:MaName.
name-case(
n
;
i
,
k
.
A
(
i
,
k
);
j
,
x
.
B
(
j
,
x
))
T
latex
Definitions
t
T
,
f
(
a
)
,
x
(
s1
,
s2
)
,
let
x
,
y
=
A
in
B
(
x
;
y
)
,
Id
,
x
:
A
.
B
(
x
)
,
hasloc(
k
;
i
)
,
b
,
Type
,
Knd
,
{
x
:
A
|
B
(
x
)}
,
x
,
y
.
t
(
x
;
y
)
,
let
i
,
k
:LocKnd =
ik
in
P
(
i
;
k
)
,
left
+
right
,
MaName
,
name-case(
n
;
i
,
k
.
A
(
i
;
k
);
j
,
x
.
B
(
j
;
x
))
,
x
:
A
B
(
x
)
Lemmas
MaName
wf
,
locknd-spread
wf2
,
Knd
wf
,
assert
wf
,
hasloc
wf
,
Id
wf
origin
T:Type, A:(i:Id
{k:Knd| 
hasloc(k;i)} T), B:(IdIdT), n:MaName.
T T:Type, A:(i:Id{k:Knd| hasloc(k;i)} T), B:(IdIdT), n:MaName.
T Tx:A. B(x)b
x,y. t(x;y)B(x)